Termination w.r.t. Q proof of TRS/secret06toList.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

Q is empty.

The TRS is overlay and locally confluent. By [15] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
LISTIFY(n, xs) → ELEM(n)
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
TOLIST(n) → LISTIFY(n, nil)
LISTIFY(n, xs) → RIGHT(n)
LISTIFY(n, xs) → LEFT(left(n))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
APPEND(cons(y, ys), x) → APPEND(ys, x)
LISTIFY(n, xs) → LEFT(n)
LISTIFY(n, xs) → RIGHT(left(n))
LISTIFY(n, xs) → ISEMPTY(n)
LISTIFY(n, xs) → ISEMPTY(left(n))
LISTIFY(n, xs) → APPEND(xs, n)
LISTIFY(n, xs) → ELEM(left(n))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
LISTIFY(n, xs) → ELEM(n)
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
TOLIST(n) → LISTIFY(n, nil)
LISTIFY(n, xs) → RIGHT(n)
LISTIFY(n, xs) → LEFT(left(n))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
APPEND(cons(y, ys), x) → APPEND(ys, x)
LISTIFY(n, xs) → LEFT(n)
LISTIFY(n, xs) → RIGHT(left(n))
LISTIFY(n, xs) → ISEMPTY(n)
LISTIFY(n, xs) → ISEMPTY(left(n))
LISTIFY(n, xs) → APPEND(xs, n)
LISTIFY(n, xs) → ELEM(left(n))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
LISTIFY(n, xs) → ELEM(n)
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)
LISTIFY(n, xs) → LEFT(left(n))
LISTIFY(n, xs) → RIGHT(n)
TOLIST(n) → LISTIFY(n, nil)
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
APPEND(cons(y, ys), x) → APPEND(ys, x)
LISTIFY(n, xs) → RIGHT(left(n))
LISTIFY(n, xs) → LEFT(n)
LISTIFY(n, xs) → ISEMPTY(n)
LISTIFY(n, xs) → APPEND(xs, n)
LISTIFY(n, xs) → ISEMPTY(left(n))
LISTIFY(n, xs) → ELEM(left(n))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 2 SCCs with 10 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND(cons(y, ys), x) → APPEND(ys, x)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

APPEND(cons(y, ys), x) → APPEND(ys, x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
APPEND(x1, x2) = APPEND(x1, x2)
cons(x1, x2) = cons(x1, x2)
y = y

Recursive path order with status [2].
Quasi-Precedence:

trivial

Status:

APPEND₂: multiset
y: multiset
cons₂: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LISTIFY(n, xs) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
IF(false, true, n, m, xs, ys) → LISTIFY(n, ys)
IF(false, false, n, m, xs, ys) → LISTIFY(m, xs)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1, x2))
left(empty)
left(node(x0, x1, x2))
right(empty)
right(node(x0, x1, x2))
elem(node(x0, x1, x2))
append(nil, x0)
append(cons(y, x0), x1)
listify(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
toList(x0)

We have to consider all minimal (P,Q,R)-chains.